L:Top List. firstn(||L||;L) ~ L 

latex

Definitions	ij, Unit, P  Q, P & Q, P  Q, T, P  Q, i<j, ||as||, Top, , ij, AB, b, b, x:A. B(x), True, t  T, Prop
Lemmas	bnot wf, assert wf, le wf, le int wf, bool wf, top wf, length wf1, lt int wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, non neg length